Iof proof for Lemma complete nat ind:
1. P :
{k}
2.
i:. (j:i. P(j)) 
P(i)
3. i :
4.
i1:i. P(i1)
P(i)
by ((BackThruHyp 2)
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n
C)) (first_tok :t) inil_term)))
C.| 9,38 |
{k}
i:. (j:i. P(j)) P(i)
i1:i. P(i1)
P(i)
by ((BackThruHyp 2)
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n
C)) (first_tok :t) inil_term)))
C.
| Definitions |  T Qx:A. B(x) |